(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)

Require Import Reals.
Require Import List.
Require Import Matrix.Mat.RMatrix.
Require Import Matrix.Mat.Matrix_Module.

Open Scope R_scope.

Lemma Rneg_mul_l: forall (x y:R),-x * y = -(x*y).
Proof. intros. ring. Qed.

Lemma Rneg_mul_r: forall (x y:R), x*-y = -(x*y).
Proof. intros. ring. Qed.

Lemma Rneg_neg_mul : forall (x y:R),-x*-y = x*y.
Proof. intros. ring. Qed.

Lemma Rsqr_x_x : forall (x:R),x*x =Rsqr x.
Proof. unfold Rsqr. reflexivity. Qed.

Lemma cos2_sin2 : forall (x:R), (cos x)²+(sin x)² = 1.
Proof. intros. rewrite Rplus_comm with (r1:=(cos x)²)(r2:=(sin x)²). apply sin2_cos2.
Qed.

(* RMat 矩阵相乘化简证明 *)
Ltac RMat_mul_simpl:=
  unfold RMatrix.Meq,M_eq;
  simpl;
  unfold RMmul,RMatrix.Mmul,Mat_mult.matrix_mul
         ,RMatrix.A,RM.Zero,RM.add,RM.mul;
  simpl;
  unfold mat_mul_mat,dl_mul_dl;
  simpl;
  rewrite ?Rmult_0_l , ?Rmult_0_r, ?Rplus_0_l , ?Rplus_0_r,
          ?Rmult_1_l , ?Rmult_1_r.


Ltac RMI_simpl:=
  unfold RM.One;
  unfold Mat_IO.dlist_i',rev;
  unfold Mat_IO.list_i; simpl.

Ltac Rtrigo_simpl:=
    rewrite  ?Rneg_neg_mul,?Rneg_mul_l, ?Rneg_mul_r, ?Rsqr_x_x; 
  rewrite ?sin2_cos2, ?cos2_sin2.

Ltac f_equal2 :=
  f_equal; f_equal.

Ltac f_equal3 :=
  f_equal; f_equal; f_equal.







